M:MsgA, x:Id, v:M.ds(x). M.init(x)?v  M.ds(x) 

latex

Definitions	IdDeq, x  dom(f), a:A fp B(a), Unit, P  Q, P & Q, , Prop, b, b, A, False, f(x), P  Q, MsgA, M.ds(x), Valtype(da;k), M.init(x)?v, x. t(x), x:A. B(x), Top, t  T, f(x)?z, Id
Lemmas	fpf-cap wf, msga wf, Id wf, ma-ds wf, fpf-ap wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-trivial-subtype-top, fpf-dom wf, bool wf, id-deq wf